chore: 📝 Links in deflist in Rocqnavi comments - #2103

@hoheinzollern @proux01 RFC: What do you think about this "feature"? This is low-tech but arguably more stable than adding custom parsing, not very user-friendly but anyway we do not expect use to write tons of documentation.

sounds good

looks good, I'm a bit worried though about stuff like [`{RV P >-> T'}`](#31c5002a151d32a5908113f99aedfaa1) because it breaks readability

it might also not be stable across edits (have you checked?)
otoh [`distribution P X`](#distribution) looks good enough, it tells me to look for the distribution symbol in the file, we could even add editor support to this kind of comments

it might also not be stable across edits (have you checked?)

The hash is created by a standard OCaml function so that should be fairly stable.

otoh [`distribution P X`](#distribution) looks good enough, it tells me to look for the distribution symbol in the file, we could even add editor support to this kind of comments

We need to think about that indeed @yoshihiro503

you can consider also a flag that fails to build the documentation if the link does not match a symbol in the file, this way you can catch any mismatch, especially for the hash-based ones.

Unfortunately, there is no "building" the documentation, it's just plain markdown interpreted by the browser when you view it. Maybe there exist tools to check links in there though?

@proux01, I mean rocqnavi builds the html page and generates the links, it can check that the anchors in the markdown sections are generated by the html rendering of the code, with a warning by default and an optional flag that fails the build if the check fails.

Sure, but that's not technically trivial since currently the markdown comment is not really parsed by rocqnavi, only copied to the html page (the markdown interpretation being done in the browser by some javascript code).

Agreed, though I think it's just a regular expressions to identify internal anchors of the form [...](#...) and to check that they are available on the generated page. Otoh my comment comes from the consideration that having hashes for anchors is not guaranteed to be stable in general: e.g. changing of the notation by adding whitespace may not alter the notation but change the hash (caveat: I don't know how those hashes are generated). I mostly care that the docs do not suddenly break because of changes in the code.

Alternative idea: if our flavor of markdown supports language-specific highlighting (e.g., like in pandoc: `{RV P >-> T}`{.rocq}) then one could trigger code formatting in these sections to get the anchors, and the result would be less cluttered. I see problems with added complexity here though, and I'm not sure it's feasible.

The anchor check could also be done with an HTML/Markdown validator at the end of the build.

Also, I checked out the sample artifact, and noticed that the link to the notation for the variance points to the wrong anchor (the local notation inside the section building it, not the global instance). This is not a great process and requires a lot of manual review.

Digging a bit, I can see that the hashes are built from the .glob files, e.g., "::form_scope:'{'_'RV'_x_'>->'_x_'}'" produces 31c5002a... via md5. One suggestion to make it both (slightly) more readable and easier to review is to use a url-friendly version of that as the key, instead of obfuscating it through hashing.

From a quick experiment across the entire MC/MCA repos, we can entirely bypass the hashing and just use the output identifiers from the .glob files, e.g.:

[`{RV P >-> T'}`](#::form_scope:'{'_'RV'_x_'>->'_x_'}')
[`'E_P[X]`](#::ereal_scope:'''E_'_x_'['_x_']')
[`'V_P[X]`](#:::'''V_'_x_'['_x_']')

with a few caveats that I'm aware of:

• round parentheses ( ) must be balanced in the notation (we have no exception to this rule)
• backslashes \ need to be doubled in order to be rendered (e.g., one needs to write [f \+ g](#::ereal_dual_scope:x_'\\+'_x) instead of [f \+ g](#::ereal_dual_scope:x_'\+'_x)).
  All the remaining notations IDs in the .glob files are url-safe.

Advantages:

• it's human readable and not dependent from the hashing
• easy to extend editors to recognize these links, as they already use the .glob file notations, no need to go back-and-forth to their hashed value
• we simplify the handling of links in rocqnavi, by just using the identifier present in the .glob file as an anchor regardless of whether it's a definition, theorem etc. or a notation.

Disadvantages:

• we expose some of the internals of how these identifiers are generated,
• which is potentially brittle if this ever changes (a quick history search shows it's been stable since 2010), but this brittleness holds equally for exposing the hashed values.

Yet another approach is to derive an simpler identifier, e.g.:

[`{RV P >-> T'}`](#{.RV._.>->._.}@form_scope)
[`'E_P[X]`](#'E_._.[._.]@ereal_scope)
[`'V_P[X]`](#'V_._.[._.])

I'm leaning against this options as it would further complicate the parser, we would need to be absolutely sure that the encoding is injective, and I'd rather push a change like this upstream to the .glob file generation if we think it's worthwhile. (I'm worried though than an encoding like this is not injective)

I don't know, I feel the hashes are nearly less disturbing when reading the source. I fear your proposition may make the links harder to copy/quote... Anyway, that's not a strong opinion, feel free to ignore it, but I feel the current PR offer is fine for now. Checking links would be nice but can be done separately.